Inference at * 1 
Iof proof for Lemma outl wf:



1. A : Type
2. B : Type
3. x : A + B
4. isl(x)
  outl(x)  A 

latex

 by ((D 3) 
CollapseTHENM (Reduce (-1))) 

latex

C1: 

C1: 3. x1 : A
C1: 4. True
C1:   outl(inl x1 )  A
C2: 

C2: 3. y : B
C2: 4. False
C2:   outl(inr y )  A
C.

Definitions

if b then t else f fi , ff, tt, isl(x), b